es:ES, e:E. isrcv(e)  (emsg(e)  sends(lnk(e);sender(e))) 

latex

Definitions	index(e), isrcv(e), E, ES, emsg(e), (x  l), x:A. B(x), i  j < k, P & Q, AB, {i..j}, A & B, Prop, l[i], sends(l;e), S  T, sender(e), lnk(e), P  Q, b, Msg, ||as||, ij, x:A. B(x), , (Msg on l), t  T
Lemmas	es-lnk wf, es-Msgl wf, es-Msg wf, es-sender wf, es-sends wf, select wf, length wf1, es-index wf, int seg wf, non neg length, le wf, es-axioms, event system wf, es-E wf, es-isrcv wf, assert wf